WebAssembly Specification

Release 1.0 (Draft, last updated Jan 23, 2018)

1. Introduction

1.1. Introduction

WebAssembly (abbreviated Wasm [1]) is a safe, portable, low-level code format designed for efficient execution and compact representation. Its main goal is to enable high performance applications on the Web, but it does not make any Web-specific assumptions or provide Web-specific features, so it can be employed in other environments as well.

WebAssembly is an open standard developed by a W3C Community Group that includes representatives of all major browser vendors.

This document describes version 1.0 of the core WebAssembly standard. It is intended that it will be superseded by new incremental releases with additional features in the future.

1.1.1. Design Goals

The design goals of WebAssembly are the following:

  • Fast, safe, and portable semantics:
    • Fast: executes with near native code performance, taking advantage of capabilities common to all contemporary hardware.
    • Safe: code is validated and executes in a memory-safe [2], sandboxed environment preventing data corruption or security breaches.
    • Well-defined: fully and precisely defines valid programs and their behavior in a way that is easy to reason about informally and formally.
    • Hardware-independent: can be compiled on all modern architectures, desktop or mobile devices and embedded systems alike.
    • Language-independent: does not privilege any particular language, programming model, or object model.
    • Platform-independent: can be embedded in browsers, run as a stand-alone VM, or integrated in other environments.
    • Open: programs can interoperate with their environment in a simple and universal manner.
  • Efficient and portable representation:
    • Compact: has a binary format that is fast to transmit by being smaller than typical text or native code formats.
    • Modular: programs can be split up in smaller parts that can be transmitted, cached, and consumed separately.
    • Efficient: can be decoded, validated, and compiled in a fast single pass, equally with either just-in-time (JIT) or ahead-of-time (AOT) compilation.
    • Streamable: allows decoding, validation, and compilation to begin as soon as possible, before all data has been seen.
    • Parallelizable: allows decoding, validation, and compilation to be split into many independent parallel tasks.
    • Portable: makes no architectural assumptions that are not broadly supported across modern hardware.

WebAssembly code is also intended to be easy to inspect and debug, especially in environments like web browsers, but such features are beyond the scope of this specification.

[1] A contraction of “WebAssembly”, not an acronym, hence not using all-caps.
[2] No program can break WebAssembly’s memory model. Of course, it cannot guarantee that an unsafe language compiling to WebAssembly does not corrupt its own memory layout, e.g. inside WebAssembly’s linear memory.

1.1.2. Scope

At its core, WebAssembly is a virtual instruction set architecture (virtual ISA). As such, it has many use cases and can be embedded in many different environments. To encompass their variety and enable maximum reuse, the WebAssembly specification is split and layered into several documents.

This document is concerned with the core ISA layer of WebAssembly. It defines the instruction set, binary encoding, validation, and execution semantics, as well as a textual representation. It does not, however, define how WebAssembly programs can interact with a specific environment they execute in, nor how they are invoked from such an environment.

Instead, this specification is complemented by additional documents defining interfaces to specific embedding environments such as the Web. These will each define a WebAssembly application programming interface (API) suitable for a given environment.

1.1.3. Dependencies

WebAssembly depends on two existing standards:

However, to make this specification self-contained, relevant aspects of the aforementioned standards are defined and formalized as part of this specification, such as the binary representation and rounding of floating-point values, and the value range and UTF-8 encoding of Unicode characters.

Note

The aforementioned standards are the authorative source of all respective definitions. Formalizations given in this specification are intended to match these definitions. Any discrepancy in the syntax or semantics described is to be considered an error.

1.2. Overview

1.2.1. Concepts

WebAssembly encodes a low-level, assembly-like programming language. This language is structured around the following concepts.

Values
WebAssembly provides only four basic value types. These are integers and IEEE 754-2008 numbers, each in 32 and 64 bit width. 32 bit integers also serve as Booleans and as memory addresses. The usual operations on these types are available, including the full matrix of conversions between them. There is no distinction between signed and unsigned integer types. Instead, integers are interpreted by respective operations as either unsigned or signed in two’s complement representation.
Instructions
The computational model of WebAssembly is based on a stack machine. Code consists of sequences of instructions that are executed in order. Instructions manipulate values on an implicit operand stack [1] and fall into two main categories. Simple instructions perform basic operations on data. They pop arguments from the operand stack and push results back to it. Control instructions alter control flow. Control flow is structured, meaning it is expressed with well-nested constructs such as blocks, loops, and conditionals. Branches can only target such constructs.
Traps
Under some conditions, certain instructions may produce a trap, which immediately aborts execution. Traps cannot be handled by WebAssembly code, but are reported to the outside environment, where they typically can be caught.
Functions
Code is organized into separate functions. Each function takes a sequence of values as parameters and returns a sequence of values as results. [2] Functions can call each other, including recursively, resulting in an implicit call stack that cannot be accessed directly. Functions may also declare mutable local variables that are usable as virtual registers.
Tables
A table is an array of opaque values of a particular element type. It allows programs to select such values indirectly through a dynamic index operand. Currently, the only available element type is an untyped function reference. Thereby, a program can call functions indirectly through a dynamic index into a table. For example, this allows emulating function pointers by way of table indices.
Linear Memory
A linear memory is a contiguous, mutable array of raw bytes. Such a memory is created with an initial size but can be grown dynamically. A program can load and store values from/to a linear memory at any byte address (including unaligned). Integer loads and stores can specify a storage size which is smaller than the size of the respective value type. A trap occurs if an access is not within the bounds of the current memory size.
Modules
A WebAssembly binary takes the form of a module that contains definitions for functions, tables, and linear memories, as well as mutable or immutable global variables. Definitions can also be imported, specifying a module/name pair and a suitable type. Each definition can optionally be exported under one or more names. In addition to definitions, modules can define initialization data for their memories or tables that takes the form of segments copied to given offsets. They can also define a start function that is automatically executed.
Embedder
A WebAssembly implementation will typically be embedded into a host environment. This environment defines how loading of modules is initiated, how imports are provided (including host-side definitions), and how exports can be accessed. However, the details of any particular embedding are beyond the scope of this specification, and will instead be provided by complementary, environment-specific API definitions.
[1] In practice, implementations need not maintain an actual operand stack. Instead, the stack can be viewed as a set of anonymous registers that are implicitly referenced by instructions. The type system ensures that the stack height, and thus any referenced register, is always known statically.
[2] In the current version of WebAssembly, there may be at most one result value.

1.2.2. Semantic Phases

Conceptually, the semantics of WebAssembly is divided into three phases. For each part of the language, the specification specifies each of them.

Decoding
WebAssembly modules are distributed in a binary format. Decoding processes that format and converts it into an internal representation of a module. In this specification, this representation is modelled by abstract syntax, but a real implementation could compile directly to machine code instead.
Validation
A decoded module has to be valid. Validation checks a number of well-formedness conditions to guarantee that the module is meaningful and safe. In particular, it performs type checking of functions and the instruction sequences in their bodies, ensuring for example that the operand stack is used consistently.
Execution

Finally, a valid module can be executed. Execution can be further divided into two phases:

Instantiation. A module instance is the dynamic representation of a module, complete with its own state and execution stack. Instantiation executes the module body itself, given definitions for all its imports. It initializes globals, memories and tables and invokes the module’s start function if defined. It returns the instances of the module’s exports.

Invocation. Once instantiated, further WebAssembly computations can be initiated by invoking an exported function on a module instance. Given the required arguments, that executes the respective function and returns its results.

Instantiation and invocation are operations within the embedding environment.

2. Structure

2.1. Conventions

WebAssembly is a programming language that has multiple concrete representations (its binary format and the text format). Both map to a common structure. For conciseness, this structure is described in the form of an abstract syntax. All parts of this specification are defined in terms of this abstract syntax.

2.1.1. Grammar Notation

The following conventions are adopted in defining grammar rules for abstract syntax.

  • Terminal symbols (atoms) are written in sans-serif font: .
  • Nonterminal symbols are written in italic font: .
  • is a sequence of class=""> <> . (This is a shortclass=""> used where <)
  • . (This is a shorthand forclass=""> where <
  • class=""> <> where <
  • Productions are written <
  • Some productions are augmented with side condclass=""> ”, that provide a shorthand for a combinatorial expansion ofclass=""> <>

2.1.2. Auxiliary Notation

When dealing with syntactic constructs the following notation is also used:

  • denotes the empty sequence.
  • denotes the leclass=""> .
  • -th class="">
  • denotes the sub-sequenceclass=""> <>.
  • denotes the same sclass=""> <
  • is replaced with denotes the flat sequence fclass=""> .

Moreover, the following class=""> class=""> <

  • The notation , where is a non-terminal symbol, is treated as a meta variable ranclass=""> (similarly for , , ).
  • When gclass=""> < occurrences oclass=""> in a sequence written are assumed to be in point-wise coclass=""> (sclass=""> , , ). This implicitly expressclass=""> <>Productions of the following form are interpreted as records that map a fixed set of fields to “values” , respectively:

    The following class=""> <

    denotes the contents of the component ofclass="">

  • denotesclass=""> component is replaced class=""> .

  • class=""> denotes the composition of two recoclass=""> <
    denotes the composition of a sequclass="">

    The update notation for sequences and records generalizes recursively to nested components accessed by “paths” :

      is sclass=""> is shoclass=""> .

      class=""> <="index-2">

      2.1.3. Vectors

      Vectors are bounded sequences of the form (or ), where the can either beclass="">

      2.2. Values

      WebAssembly programs operate on primitive numeric values. Moreover, in the definition of programs, immutable sequences of values occur to represent more complex data, such as text strings or other vectors.

      2.2.1. Bytes

      The simplest form of value are raw uninterpreted bytes. In the abstract syntax they are represented as hexadecimal literals.

      2.2.1.1. Conventions
      • The meta variable ranges over bytes.
      • Bytes are sometimes interpreted as natural numbers .

      2.2.2. Integers

      Different classes of integers with different value ranges are distinguished by their bit width and by whether they are unsigned or signed.

      convert them to signed based on a two’s complement interpretation.

      Note

      The main integer types occurring in this specification are , class=""> , class=""> , class=""> , class=""> , , class=""> , class=""> . class=""> <#syntax-float">floating-point numbers.

      2.2.2.1. Conventions
      • The meta variables range over integers.
      • Numbers may be denoted by simple arithmetics, as in theclass=""> from sequences like , the latter is distinguished with parentheclass="">
      class="">

      2.2.3. Floating-Point

      Floating-point data represents 32 or 64 bit values that correspond to the respective binary formats of the IEEE 754-2008 standard (Section 3.3).

      Every value has a sign and a magnitude. Magnitudes can either be expressed as normal numbers of the form , where is the exponent and is , or as a subnormal number where the exponent is fixed class=""> is ; among the subnormals are positive and negative zero values. Siclass=""> , where is the bit width of

      Poclass=""> (infinity) and < a number). NaN values have class=""> binary representation. No distinction is made between signalling and quiet NaNs.

      <
      <}{lclllllcl} \href{../syntax/valuclass="">

      A canonical NaN is a floating-point value :

      with <
      class=""> Note

      In the abstract syntax, subnormals are distinguished by the leading 0 of the significand. The exponent of subnormals has the same value as the smallest possible exponent of a normal number. Only in the binary representation the exponent of a subnormal is encoded differently than the exponent of any normal number.

      2.2.3.1. Conventions
      • The meta variable ranges over floating-point values where clear from context.
      class=""> <

      2.2.4. Names

      Names are sequences of scalar code points as defined by Unicode (Section 2.4).

      binary format, the lengths of a name is bounded by the length of its UTF-8 encoding.

      2.2.4.1. Convention
      • Code points are sometimes used interchangeably with natural numbers .

      2.3. Types

      Various entitites in WebAssembly are classified by types. Types are checked during validation, instantiation, and possibly execution.

      2.3.1. Value Types

      Value types classify the individual values that WebAssembly code can compute with and the values that a variable accepts.

      The types and single and double precision, as defined by the IEEE 754-2008 standard (Section 3.3).

      2.3.1.1. Conventions
      • The meta variable ranges over value types where clear from context.
      • The notation bit width of a value type. That is, <

        2.3.2. Result Types

        Result types classify the result of executing instructions or blocks, which is a sequence of values.

        <

        In the current version of WebAssembly, at most one value is allowed as a result. However, this may be generalized to sequences of values in future versions.

      2.3.3. Function Types

      Function types classify the signature of functions, mapping a vector of parameters to a vector of results.

      <

      In the current version of WebAssembly, the length of the result type vector of a valid function type may be at most . This restriction may be removed in future versions.

      class="">

      2.3.4. Limits

      Limits classify the size range of resizeable storage associated with memory types and table types.

      2.3.5. Memory Types

      Memory types classify linear memories and their size range.

      page size.

      2.3.6. Table Types

      Table types classify tables over elements of element types within a size range.

      < are given in numbers of entries.

      The element type is the infinite union of all . A table of that type thus contains references to functions of heterogeneous type.

      Note

      In future versions of WebAssembly, additional element types may be introduced.

      2.3.7. Global Types

      Global types classify global variables, which hold a value and can either be mutable or immutable.

      <

      2.3.8. External Types

      External types classify imports and external values with their respective types.

      2.3.8.1. Conventions

      The following auxiliary notation is defined for sequences of external types. It filters out entries of a specific kind in an order-preserving fashion:

      • 2.4. Instructions

        WebAssembly code consists of sequences of instructions. Its computational model is based on a stack machine in that instructions manipulate values on an implicit operand stack, consuming (popping) argument values and producing (pushing) result values.

        Note

        In the current version of WebAssembly, at most one result value can be pushed by a single instruction. This restriction may be lifted in future versions.

        In addition to dynamic operands from the stack, some instructions also have static immediate arguments, typically indices or type annotations, which are part of the instruction itself.

        Some instructions are structured in that they bracket nested sequences of instructions.

        The following sections group instructions into a number of different categories.

        2.4.1. Numeric Instructions

        Numeric instructions provide basic operations over numeric values of specific type. These operations closely match respective operations available in hardware.

        value type. For each type, several subcategories can be distinguished:

        • Constants: return a static constant.
        • Unary Operators: consume one operand and produce one result of the respective type.
        • Binary Operators: consume two operands and produce one result of the respective type.
        • Tests: consume one operand of the respective type and produce a Boolean integer result.
        • Comparisons: consume two operands of the respective type and produce a Boolean integer result.
        • Conversions: consume a value of one type and produce a result of another (the source type of the conversion is the one after the “”).

        Some integer instructions come in two flavours, whereclass=""> distinguishes whether the operands are to beclass=""> interpreted as unsigned or signed integers. For the other integer instructions, the use of two’s complement for the signed interpretation means that they behave the same regardless of signedness.

        2.4.1.1. Conventions

        Occasionally, it is convenient to group operators together according to the following grammar shorthands:

        <="syntax-instr-parametric">

        2.4.2. Parametric Instructions

        Instructions in this group can operate on operands of any value type.

        operator simply throws away class=""> operator selects one of itclass=""> <

        2.4.3. Variable Instructions

        Variable instructions are concerned with the access to local or global variables.

        instruction is like but also returns its argclass=""> <

        2.4.4. Memory Instructions

        Instructions in this group are concerned with linear memory.

        and <>value types. They all take a memory immediate that contains an address offset < loads and stores can optionally specify a storage size that is smaller than the bit width of the respective value type. In the case of loads, a sign extension mode is then required to select appropriate behavclass=""> effective address that is the zero-based index at which the memory is accessed. All values are read and written in little endian byte order. A trap results if any of the accessed memory bytes lies outside the address range implied by the memory’s current size.

        Note

        Future version of WebAssembly might provide memory instructions with 64 bit address ranges.

        The instruction returns tclass=""> instruction grows memoryclass=""> page size.

        Note

        In the current version of WebAssembly, all memory instructions implicitly operate on memory index . This restriction may be lifted in future versions.

        class="">

        2.4.5. Control Instructions

        Instructions in this group affect the flow of control.

        class=""> instruction causes an unclass=""> <.

        The , < structured <>, terminated with, or separated by, or result type.

        Each structured control instruction introduces an implicit label. Labels are targets for branch instructions that reference them with label indices. Unlike with other index spaces, indexing of labels is relative by nesting depth, that is, label refers to the innermost structured control instruction enclosing the referring branch instruction, wclass=""> within the associated structured control instruction. This also implies that branches can only be directed outwards, “breaking” from the block of the control construct they target. The exact effect depends on that control construct. In case of or , reclass=""> . In case of backward jump class=""> <

        Note

        This enforces structured control flow. Intuitively, a branch targeting a or behaves like a performs an unconditional branch,class=""> performs a conditional branchclass=""> performs an indirect brancclass=""> instruction is a shortcut forclass=""> unwinds the operand stack up to the height where the targeted structured control instruction was entered. However, forward branches that target a control instruction with a non-empty result type consume matching operands first and push them back on the operand stack after unwinding, as a result for the terminated structured instruction.

        The instruction invokes another , consuming the necessary arguments from the stack and returning the result values of the call. The instruction calls a fclass=""> table. Since tables may contain function elements of heterogeneous type , the callee is dynamically checked againclass=""> function type indexed by the instruction’s immediate, and the call aborted with a trap if it does not match.

        Note

        In the current version of WebAssembly, implicitly operates oclass=""> index . This restriction may be lifted in future versions.

        class="">

        2.4.6. Expressions

        Function bodies, initialization values for globals, and offsets of element or data segments are given as expressions, which are sequences of instructions terminated by an marker.

        restricts expressions to be constant, which limits the set of allowable instructions.

        2.5. Modules

        WebAssembly programs are organized into modules, which are the unit of deployment, loading, and compilation. A module collects definitions for types, functions, tables, memories, and globals. In addition, it can declare imports and exports and provide initialization logic in the form of data and element segments or a start function.

        2.5.1. Indices

        Definitions are referenced with zero-based indices. Each class of definition has its own index space, as distinguished by the following classes.

        <, tables, memories and globals includes respective imports declared in the same module. The indices of these imports precede the indices of other definitions in the same index space.

        The index space for locals is only accessible inside a function and includes the parameters and local variables of that function, which precede the other locals.

        Label indices reference structured control instructions inside an instruction sequence.

        2.5.1.1. Conventions
        • The meta variable ranges over label indices.
        • The meta variables rclass="">
        class=""> <

        2.5.2. Types

        The component of a module defines a vector of class=""> function types.

        All function types used in a module must be defined in this component. They are referenced by type indices.

        Note

        Future versions of WebAssembly may add additional forms of type definitions.

        2.5.3. Functions

        The component of a module defines a vector of class=""> type defined in the module. The parameters of the function are referenced through 0-based local indices in the function’s body.

        The declare a vector of mutable local variablesclass=""> < internal" href="#syntax-localidx">local indices in the function’s body. The index of the first local is the smallest index not referencing a parameter.

        The is an result type.

        Functions are referenced through function indices, starting with the smallest index not referencing a function import.

        2.5.4. Tables

        The component of a module defines a vector ofclass=""> table type:

        <#syntax-elemtype">element type. The size in the , if present, restricts the size to which it caclass=""> element segments.

        Tables are referenced through table indices, starting with the smallest index not referencing a table import. Most constructs implicitly reference table index .

        <

        In the current version of WebAssembly, at most one table may be defined or imported in a single module, and all constructs implicitly reference this table . This restriction may be lifted in future versions.

        class="">

        2.5.5. Memories

        The component of a module defines a vector of memory type:

        size in the , if present, restricts the size to which it caclass=""> page size.

        Memories can be initialized through data segments.

        Memories are referenced through memory indices, starting with the smallest index not referencing a memory import. Most constructs implicitly reference memory index .

        <

        In the current version of WebAssembly, at most one memory may be defined or imported in a single module, and all constructs implicitly reference this memory . This restriction may be lifted in future versions.

        class="">

        2.5.6. Globals

        The component of a module defines a vector oclass=""> global type. Its also specifies whether a global is immutablclass=""> value given by a initializer expression.

        Globals are referenced through global indices, starting with the smallest index not referencing a global import.

        2.5.7. Element Segments

        The initial contents of a table is uninitialized. The component of a module defines a vector of vector of elements.

        expression.

        Note

        In the current version of WebAssembly, at most one table is allowed in a module. Consequently, the only valid is . class="">

        2.5.8. Data Segments

        The initial contents of a memory are zero bytes. The component of a module defines a vector of vector of bytes.

        expression.

        Note

        In the current version of WebAssembly, at most one memory is allowed in a module. Consequently, the only valid is .

        class=""> class="">

        2.5.9. Start Function

        The component of a module optionally declares class=""> <-ref">function index of a start function that is automatically invoked when the module is instantiated, after tables and memories have been initialized.

        2.5.10. Exports

        The component of a module defines a set of instantiated.

        name. Exportable definitions are functions, tables, memories, and globals, which are referenced through a respective descriptor.

        Note

        In the current version of WebAssembly, only immutable globals may be exported.

        2.5.10.1. Conventions

        The following auxiliary notation is defined for sequences of exports, filtering out indices of a specific kind in an order-preserving fashion:

        • 2.5.11. Imports

          The component of a module defines a set of <.html#exec-instantiation">instantiation.

          name space, consisting of a name and a unique functions, tables, memories, and globals. Each import is specified by a descriptor with a respective type that a definition provided during instantiation is required to match.

          Every import defines an index in the respective index space. In each index space, the indices of imports go before the first index of any definition contained in the module itself.

          Note

          In the current version of WebAssembly, only immutable globals may be imported.

        3. Validation

        3.1. Conventions

        Validation checks that a WebAssembly module is well-formed. Only valid modules can be instantiated.

        Validity is defined by a type system over the abstract syntax of a module and its contents. For each piece of abstract syntax, there is a typing rule that specifies the constraints that apply to it. All rules are given in two equivalent forms:

        1. In prose, describing the meaning in intuitive form.
        2. In formal notation, describing the rule in mathematical form. [1]

        Note

        The prose and formal rules are equivalent, so that understanding of the formal notation is not required to read this specification. The formalism offers a more concise description in notation that is used widely in programming languages semantics and is readily amenable to mathematical proof.

        In both cases, the rules are formulated in a declarative manner. That is, they only formulate the constraints, they do not define an algorithm. The skeleton of a sound and complete algorithm for type-checking instruction sequences according to this specification is provided in the appendix.

        3.1.1. Contexts

        Validity of an individual definition is specified relative to a context, which collects relevant information about the surrounding module and the definitions in scope:

        • Types: the list of types defined in the current module.
        • Functions: the list of functions declared in the current module, represented by their function type.
        • Tables: the list of tables declared in the current module, represented by their table type.
        • Memories: the list of memories declared in the current module, represented by their memory type.
        • Globals: the list of globals declared in the current module, represented by their global type.
        • Locals: the list of locals declared in the current function (including parameters), represented by their value type.
        • Labels: the stack of labels accessible from the current position, represented by their result type.
        • Return: the return type of the current function, represented as a result type.

        In other words, a context contains a sequence of suitable types for each index space, describing each defined entry in that space. Locals, labels and return type are only used for validating instructions in function bodies, and are left empty elsewhere. The label stack is the only part of the context that changes as validation of an instruction sequence proceeds.

        It is convenient to define contexts as records with abstract syntax:

        <

        The fields of a context are not defined as vectors, since their lengths are not bounded by the maximum vector size.

        In addition to field access the following notation is adopted for manipulating contexts:

          denotes the same context as but with the elemclass=""> <> component sequence. Note

          This notation is defined to prepend not append. It is only used in situations where the original is either empty or is label index space is indexed relatively, that is, in reverse order of addition.

        3.1.2. Prose Notation

        Validation is specified by stylised rules for each relevant part of the abstract syntax. The rules not only state constraints defining when a phrase is valid, they also classify it with a type. The following conventions are adopted in stating these rules.

        3.1.3. Formal Notation

        Note

        This section gives a brief explanation of the notation for specifying typing rules formally. For the interested reader, a more thorough introduction can be found in respective text books. [2]

        The proposition that a phrase has a respective type is written class=""> . To expreclass=""> < complete form is a judgement holds under the assumptions encodeclass=""> .

        The fclass=""> deduction rules. Every rule has the following general form:

        axioms whose conclusion holds unconditionally. The conclusion always is a judgment , and there is one respective rule for each relevant construct

        Note

        For example, the typing rule for the can be typed as follows:class=""> local index exists in the context. The instruction produces a value of its respective type does not exist then the premise does noclass=""> structured instruction requires a recursive rule, where the premise is itself a typing judgement:

        instruction is only valid whenclass=""> . If so, then the with the additional label information for the premise.

        [1] The semantics is derived from the following article: Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. Bringing the Web up to Speed with WebAssembly. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017.
        [2] For example: Benjamin Pierce. Types and Programming Languages. The MIT Press 2002

        3.2. Types

        Most types are universally valid. However, restrictions apply to function types as well as the limits of table types and memory types, which must be checked during validation.

      3.2.3. Table Types

      3.2.3.1.
    • The limits must be valid
      <

      3.2.4. Memory Types

      3.2.4.1. must be valid
      <

      3.3. Instructions

      Instructions are classified by function types that describe how they manipulate the that an instruction pops off and the provided output stack with result values of types that it pushes class="">

      Note

      class=""> has type . Such a sequence has a if the accumulative effect of executing the instructions is consuming vclass=""> .

      For some inclass=""> < are called polymorphic. Two degrees of polymorphism can be distinguished:

    <.3" id="-tmathsfhref-syntax-instructionshtmlsyntax-binopmathitbinop">3.3.1.3. .
    <1.4" id="-tmathsfhref-syntax-instructionshtmlsyntax-testopmathittestop">3.3.1.4. . class=""> <.5" id="-tmathsfhref-syntax-instructionshtmlsyntax-relopmathitrelop">3.3.1.5. . class=""> < id="-t_2mathsfhref-syntax-instructionshtmlsyntax-cvtopmathitcvtop-t_1">3.3.1.6. .

    3.3.2. Parametric Instructions

    3.3.2.1. , for any
    <" id="-href-syntax-instructionshtmlsyntax-instr-parametricmathsfselect">3.3.2.2. , for any
    and <

    3.3.3. Variable Instructions

    3.3.3.1. must be defined in the context.
  • Let bclass=""> <="std std-ref">value type .
  • Then the instruction is valid with type <
    <.3.2" id="-href-syntax-instructionshtmlsyntax-instr-variablemathsfset_localx">3.3.3.2. must be defined in the context.
  • Let bclass=""> <="std std-ref">value type .
  • Then the instruction is valid with type <
    <.3.3" id="-href-syntax-instructionshtmlsyntax-instr-variablemathsftee_localx">3.3.3.3. must be defined in the context.
  • Let bclass=""> <="std std-ref">value type .
  • Then the instruction is valid with type <
    <3.3.4" id="-href-syntax-instructionshtmlsyntax-instr-variablemathsfget_globalx">3.3.3.4. < global must be defined in the context.
  • Let .
  • Then the instruction is valid with type <
  • Let .
  • The mutability . class=""> <

    3.3.4. Memory Instructions

    3.3.4.1. <
    • The memory must be defined in the context.
    • The alignment must not class=""> <> divided by .
    • Then the instruction is valid with type .
    class=""> <" id="-tmathsfhref-syntax-instructionshtmlsyntax-instr-memorymathsfloadnmathsf_href-syntax-instructionshtmlsyntax-sxmathitsxhref-syntax-instructionshtmlsyntax-memargmathitmemarg">3.3.4.2.
    • The memory must be defined in the context.
    • The alignment must not class=""> .
    class=""> 3.3.4.3. <
    • The memory must be defined in the context.
    • The alignment must not class=""> <> divided by .
    • Then the instruction is valid with type .
    class=""> <4" id="-tmathsfhref-syntax-instructionshtmlsyntax-instr-memorymathsfstorenhref-syntax-instructionshtmlsyntax-memargmathitmemarg">3.3.4.4. class=""> <
    • The memory must be defined in the context.
    • The alignment must not class=""> .
    class=""> <="3.3.4.5" id="-href-syntax-instructionshtmlsyntax-instr-memorymathsfcurrent_memory">3.3.4.5. must be defined in the context.
  • Then the instruction is valid with typeclass=""> . class=""> <.3.4.6" id="-href-syntax-instructionshtmlsyntax-instr-memorymathsfgrow_memory">3.3.4.6. must be defined in the context.
  • Then the instruction is valid with typeclass="">

    3.3.5. Control Instructions

    3.3.5.1. .
    <.3.5.2" id="-href-syntax-instructionshtmlsyntax-instr-controlmathsfunreachable">3.3.5.2. , for any sequences of and .
    instruction is <
    3.3.5.6. must be defined in the context.
  • Let result type .
  • Then the instruction is valid with type , for any sequences of and .
    instruction is <
    3.3.5.7. < must be defined in the context.
  • Let result type .
  • Then the instruction is valid with type . class=""> <5.8" id="-href-syntax-instructionshtmlsyntax-instr-controlmathsfbr_tablelastl_n">3.3.5.8. must be defined in the context.
  • Let result type .
  • For all in class=""> must be . class=""> , for any sclass=""> and .
    instruction is <
    3.3.5.10. must be defined in the context.
  • Then the instruction is valid with typclass=""> .
  • Let be the .
  • The class=""> must be
  • Let class=""> .
  • Then the instruction is valid with type . class="">

    3.3.6. Instruction Sequences

    Typing of instruction sequences is defined recursively.

    3.3.6.1. Empty Instruction Sequence:
  • <

    3.3.7. Expressions

    Expressions are classified by .

    3.3.7.1. <
    <
    3.3.7.2. Constant Expressions
    • In a constant expression all instrucclass=""> < A constant instruction <> must be:
      • either of the form ,
      • or of the form < xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxclass=""> .
    < expression may be extended in future versions of WebAssembly.

    3.4. Modules

    Modules are valid when all the components they contain are valid. Furthermore, most definitions are themselves classified with a suitable type.

    <

    3.4.2. Tables

    Tables are classified by

    3.4.2.1. <="simple">
  • The table type must be .
    <

    3.4.3. Memories

    Memories are classified by <" id="id3④">

    3.4.3.1.
  • The memory type must be < with type .
    • The table must be defined in the context.
    • Let be the .
    • The class=""> must be result type .
    • The expression in , the function class=""> <

      3.4.6. Data Segments

      Data segments are not classified by any type.

      class=""> 3.4.6.1.
    • The memory must be defined in the context.
    • The expression < class="reference internal" href="index.html#valid-expr"> result type .
    • The expression <
    <

    3.4.7. Start Function

    Start function declarations are not classified by any type.

  • The type of < xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxclass=""> <

    3.4.8. Exports

    Exports and export descriptions

    3.4.8.1.
  • Then the export description is valid wclass=""> external type . class=""> 3.4.8.3. must be defined in the context.
  • Then the export description is valid class=""> external type . class=""> 3.4.8.4. must be defined in the context.
  • Then the export description is valid wiclass=""> external type . class=""> 3.4.8.5. < xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx/span> must be defined in the context.
  • Let .
  • The mutability . class=""> . class="">

    3.4.9. Imports

    Imports and import descriptions

    3.4.9.1.
    class=""> 3.4.9.5. class=""> <

    3.4.10. Modules

    Modules are classified by their mapping from the external types of their imports to those of their exports.

    A module is entirely closed, that is, its components can only refer to definitions that appear in the module itself. Consequently, no initial context is required. Instead, the context for validation of the module’s content is constructed from the definitions in the module.

    • Letclass=""> be the module to validate.
    • Let <="std std-ref">context where:
        is <
      • concatenated class=""> concatenatedclass=""> <> concatenated wclass=""> concatenateclass=""> be theclass=""> <-ref">context where is the sequence and all othclass=""> < xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx/span> in <="reference inteclass=""> must be in < class="std std-ref">valid function type .
      • For each validclass=""> table type .
      • For each valid <">memory type .
      • For each <
      • For each valid in valid is non-empty, then must be in vaclass=""> external type .
      • For each vaclass=""> external type .
    • The length of .
    • The length of must not be larger than .
    • All export names must be different. class=""> of the imports, in index order.
    • Let of the exports, in index order.
    • Then the module is valid with external types context in this rule is recursive: it depends on the outcome of validation of the function, table, memory, and global definitions contained in the module, wclass=""> < on . However, this recursion is just a specification device. All types needed to construct can easily be determined fromclass="">

      Globalclass=""> < recursive. The effect of defining the limited context for validating the module’s globals is that their initialization expressions can only access imported globals and nothing else.

      Note

      The restriction on the number of tables and memories may be lifted in future versions of WebAssembly.

  • 4. Execution

    4.1. Conventions

    WebAssembly code is executed when instantiating a module or invoking an exported function on the resulting module instance.

    Execution behavior is defined in terms of an abstract machine that models the program state. It includes a stack, which records operand values and control constructs, and an abstract store containing global state.

    For each instruction, there is a rule that specifies the effect of its execution on the program state. Furthermore, there are rules describing the instantiation of a module. As with validation, all rules are given in two equivalent forms:

    1. In prose, describing the execution in intuitive form.
    2. In formal notation, describing the rule in mathematical form. [1]

    Note

    As with validation, the prose and formal rules are equivalent, so that understanding of the formal notation is not required to read this specification. The formalism offers a more concise description in notation that is used widely in programming languages semantics and is readily amenable to mathematical proof.

    4.1.1. Prose Notation

    Execution is specified by stylised, step-wise rules for each instruction of the abstract syntax. The following conventions are adopted in stating these rules.

    • The execution rules implicitly assume a given store .
    • The execution rules also assume the presence of an implicit that is modified by pushing or popping values, labels, and frames.
    • Certain rules require the stack to contain at least one frame. The most recent frame is referred to as the current frame.
    • Both the store and the current frame are mutated by replacing some of its components. Such replacement is assumed to apply globally.
    • The execution of an instruction may trap, in which case the entire computation is aborted and no further modifications to the store are performed by it. (Other computations can still be initiated afterwards.)
    • The execution of an instruction may also end in a jump to a designated target, which defines the next instruction to execute.
    • Execution can enter and exit instruction sequences that form blocks.
    • Instruction sequences are implicitly executed in order, unless a trap or jump occurs.
    • In various places the rules contain assertions expressing crucial invariants about the program state.

    4.1.2. Formal Notation

    Note

    This section gives a brief explanation of the notation for specifying execution formally. For the interested reader, a more thorough introduction can be found in respective text books. [2]

    The formal execution rules use a standard approach for specifying operational semantics, rendering them into reduction rules. Every rule has the following general form:

    A configurclass=""> deterministic. WebAssembly has only very few exceptions to this, which are noted explicitly in this specification.

    For WebAssembly, a configuration typically is a tuple consisting of the current call frame of the cuclass=""> < the sequence of instructions later.)

    To avoid unnecessary clutter, the store and the frame are omitted from reduction rules that do not touch them.

    There is no separate repreclass=""> < class="reference internal"class=""> stack. Instead, it is conveniently represented as part of the configuration’s instruction sequence. In particular, values are defined to coincide with instructions, and a sequence of Note

    For example, the reduction rule for the instruction can be giveclass=""> instruction. This can be interpreted as popping two value off the stack and puclass="">

    frames are similarly defined to be part of an instruction sequence.

    The order of reduction is determined by the definition of an appropriate evaluation context.

    Reduction terminates when no more reduction rules are applicable. Soundness of the WebAssembly type system guarantees that this is only the case when the original instruction sequence has either been reduced to a sequence of instructions, which can be interpreted as the trap occurred.

    Note

    For example, the following instruction sequence,

    .

    class=""> <> < [1] The semantics is derived from the following article: Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. Bringing the Web up to Speed with WebAssembly. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017.
    [2] For example: Benjamin Pierce. Types and Programming Languages. The MIT Press 2002

    4.2. Runtime Structure

    Store, stack, and other runtime structure forming the WebAssembly abstract machine, such as values or module instances, are made precise in terms of additional auxiliary syntax.

    4.2.1. Values

    WebAssembly computations manipulate values of the four basic value types: integers and floating-point data of 32 or 64 bit width each, respectively.

    In most places of the semantics, values of different types can occur. In order to avoid ambiguities, values are therefore represented with an abstract syntax that makes their type explicit. It is convenient to reuse the same notation as for the instructions producing them:class=""> 4.2.2. Results

  • A result is the outcome of a computation. It is either a sequence of values or a trap.

    4.2.3. Store

    The store represents all global state that can be manipulated by WebAssembly programs. It consists of the runtime representation of all instances of functions, tables, memories, and globals that have been allocated during the life time of the abstract machine. [1]

    Syntactically, the store is defined as a record listing the existing instances of each category:

    [1] In practice, implementations may apply techniques like garbage collection to remove objects from the store that are no longer referenced. However, such techniques are not semantically observable, and hence outside the scope of this specification.
    4.2.3.1. Convention
    • The meta variable ranges over stores where clear from context.

    4.2.4. Addresses

    Function instances, table instances, memory instances, and global instances in the store are referenced with abstract addresses. These are simply indices into the respective store component.

    < store objects corresponding to their addresses, even where this identity is not observable from within WebAssembly code itself (such as for function instances or immutable globals).

    Note

    Addresses are dynamic, globally unique references to runtime objects, in contrast to indices, which are static, module-local references to their original definitions. A memory address denotes the abstract address of a memory instance in the store, not an offset inside a memory instance.

    4.2.5. Module Instances

    A module instance is the runtime representation of a module. It is created by instantiating a module, and collects runtime representations of all entities that are imported, defined, or exported by the module.

    indices. Function instances, table instances, memory instances, and global instances are referenced with an indirection through their respective addresses in the store.

    It is an invariant of the semantics that all export instances in a given module instance have different names.

    4.2.6. Function Instances

    A function instance is the runtime representation of a function. It effectively is a closure of the original function over the runtime module instance of its originating module. The module instance is used to resolve references to other definitions during execution of the function.

    <" href="index.html#syntax-import">import. The definition and behavior of host functions are outside the scope of this specification. For the purpose of this specification, it is assumed that when invoked, a host function behaves non-deterministically, but within certain constraints that ensure the integrity of the runtime.

    Note

    Function instances are immutable, and their identity is not observable by WebAssembly code. However, the embedder might provide implicit or explicit means for distinguishing their addresses.

    4.2.7. Table Instances

    A table instance is the runtime representation of a table. It holds a vector of function elements and an optional maximum size, if one was specified in the table type at the table’s definition site.

    Each function element is either empty, representing an uninitialized table entry, or a function address. Function elements can be mutated through the execution of an element segment or by external means provided by the embedder.

    Other table elements may be added in future versions of WebAssembly.

    4.2.8. Memory Instances

    A memory instance is the runtime representation of a linear memory. It holds a vector of bytes and an optional maximum size, if one was specified at the definition site of the memory.

    memory type, the maximum size in a memory iclass=""> class=""> memory instructions, the execution of a data segment, or by external means provided by the embedder.

    It is an invariant of the semantics that the length of the byte vector, divided by page size, never exceeds the maximum size, if present.

    4.2.9. Global Instances

    A global instance is the runtime representation of a global variable. It holds an individual value and a flag indicating whether it is mutable.

    embedder.

    4.2.10. Export Instances

    An export instance is the runtime representation of an export. It defines the export’s name and the associated external value.

    < class="secno">4.2.11. External Values

    An external value is the runtime representation of an entity that can be imported or exported. It is an address denoting either a function instance, table instance, memory instance, or global instances in the shared store.

    < href="#conventions①⑨">

    The following auxiliary notation is defined for sequences of external values. It filters out entries of a specific kind in an order-preserving fashion:

    • <12">

      4.2.12. Stack

      Besides the store, most instructions interact with an implicit stack. The stack contains three kinds of entries:

      These entries can occur on the stack in any order during the execution of a program. Stack entries are described by abstract syntax as follows.

      Note

      It is possible to model the WebAssebmly semantics using separate stacks for operands, control constructs, and calls. However, because the stacks are interdependent, additional book keeping about associated stack heights would be required. For the purpose of this specification, an interleaved representation is simpler.

      4.2.12.1. Values

      Values are represented by themselves.

      4.2.12.2. Labels

      Labels carry an argument arity and their associated branch target, which is expressed syntactically as an instruction sequence:

      class=""> <>
      <

      For example, a loop label has the form

      class="">

      When branching, the empty continuation ends the targeted block, such that execution can proceed with consecutive instructclass="">

      4.2.12.3. Frames

      Activation frames carry the return arity of the respective function, hold the values of its locals (including arguments) in the order corresponding to their static local indices, and a reference to the function’s own module instance:

      4.2.12.4. Conventions
      • The meta variable ranges over labels where clear from context.
      • The meta variable ranges over frames where clear from context.
      <

      Note

      In the currentclass=""> . This may be generalized in future versions.

      4.2.13. Administrative Instructions

      Note

      This section is only relevant for the formal notation.

      In order to express the reduction of traps, calls, and control instructions, the syntax of instructions is extended to include the following administrative instructions:

      instruction, signalling abrupt termination.

      The instructionclass=""> function instance, iclass=""> < class="std std-ref">address. It unifies the handling of different forms of calls.

      The and instructions perform initialization of < and segments during module instantiation.

      Note

      The reason for splitting instantiation into individual reduction steps is to provide a semantics that is compatible with future extensions like threads.

      The and instructions model “on the stack”. Moreover, the administrative syntax maintains the nesting structure of the original structured control instruction or function body and their instruction sequences with an marker. That way, the end of the inner instruction sequence is known when part of an outer sequence.

      reduction rule for is:

      instructions representing the resulting values – then the insclass=""> <#exec-label">reduction rule:

      class="">
      4.2.13.1. Block Contexts

      In order to specify the reduction of branches, the following syntax of block contexts is defined, indexed by the count of labels surrounding the hole:

      return instruction.

      Note

      For example, the reduction of a simple branch can be defined as follows:

      label index , which corresponds to the number of surrounding instructions that must be hopped over – which is exactly the count encoded in the iclass="">
      class="">
      4.2.13.2. Configurations

      A configuration consists of the current store and an executing thread.

      A thread is a computation over instructions that operates relative to a current frame referring to the home module instance that the computation runs in.

      4.2.13.3. Evaluation Contexts

      Finally, the following definition of evaluation context and associated structural rules enable reduction inside instruction sequences and administrative forms as well as the propagation of traps:

      values or to a .

      Note

      For example, the following instruclass="">

    • The meta variable is used to range over (class=""> <>magnitudes, excluding or .

    • The notation denotes the inverse of aclass=""> < , with the usual mathematical definiclass=""> <

      class=""> 4.3.1. Representations

      Numbers have an underlying binary representation as a sequence of bits:

      4.3.1.1. Integers

      Integers are represented as base two unsigned numbers:

      class=""> <
      <
      4.3.1.2. Floating-Point

      Floating-point values are represented in the respective binary format defined by IEEE 754-2008 (Section 3.4):

      <> < id="storage①">4.3.1.3. Storage

      When a number is stored into memory, it is converted into a sequence of bytes in little endian byte order:

      <

      4.3.2. Integer Operations

      4.3.2.1. Sign Interpretation

      Integer operators are defined on values. Operators that use a signed interpretation convert the value using the following definition, which takes the two’s compleclass=""> ):

      4.3.2.2. Boolean Interpretation

      The integer result of predicates – i.e., tests and relational operators – is defined with the help of the following auxiliary function producing the value or depending on a condition.

      4.3.2.3.
      • Return the class=""> modulo .
      class=""> <
      class=""> 4.3.2.4.
      • Return the class=""> modulo .
      class=""> <
      class=""> 4.3.2.5.
      • Return the class=""> modulo .
      class=""> <
      class=""> 4.3.2.6.
      • Ifclass=""> < is undefined.
      • Else, return the result of dividing by , truncated toward zero. class=""> <
        .

      4.3.2.7.
      • Leclass=""> signed interpretation of .
      • Let be the signed interpretation of . class=""> is , then the result is undefined.
      • Else if divided by , then class=""> by , truncated toward zerclass=""> < . Besides division by , the result of is not representable as an -bit signed integer.

      4.3.2.8.
      • Ifclass=""> < is undefined.
      • Else, return the remainder of dividing by .
      class=""> <.

      As long as both operators are defined, it holds that .

      4.3.2.9.
      • Leclass=""> signed interpretation of .
      • Let be the signed interpretation of . class=""> is , then the result is undefined.
      • Else, return the remainder of dividing by , with the sign of the diclass="">
      <.

      As long as both operators are defined, it holds that .

      4.3.2.10.
      • Return the class=""> .
      <">4.3.2.11.
      • Return the bitwclass=""> .
      4.3.2.12.
      • Return the class=""> .
      4.3.2.13.
      • Let .
      • Return the result of shifting left by bits, modulo . class=""> <
        4.3.2.14.
        • Leclass=""> .
        • Return the result of shifting right by bits, extended wclass=""> bclass=""> 4.3.2.15.
          • Leclass=""> .
          • Return the result of shifting right by bits, extended wclass=""> <
          class=""> <="secno">4.3.2.16.
          • Let .
          • Return the result of rotating left by bits. class=""> <
            <="secno">4.3.2.17.
            • Let .
            • Return the result of rotating right by bits. class=""> <
              <4.3.2.18.
              • Return the count of leadclass=""> is .
              class=""> <4.3.2.19.
              • Return the count of traiclass=""> < trailing zeros if is .
              class=""> <="secno">4.3.2.20.
              • Return the cclass=""> <
                class=""> <4.3.2.21.
                • Return otherwise.
                <
                4.3.2.22.
                • Return , otherwise.
                4.3.2.23.
                • Return , otherwise.
                <="secno">4.3.2.24.
                • Returnclass=""> , otherwise.
                <="secno">4.3.2.25.
                • Let signed interpretation of .
                • Let be the signed interpretation of . class=""> if is less than , otherwise.
                class=""> <="secno">4.3.2.26.
                • Returnclass=""> , otherwise.
                <="secno">4.3.2.27.
                • Let signed interpretation of .
                • Let be the signed interpretation of . class=""> if is greater than , otherwise.
                class=""> <="secno">4.3.2.28.
                • Returnclass=""> , otherwise.
                <="secno">4.3.2.29.
                • Let signed interpretation of .
                • Let be the signed interpretation of . class=""> if is less than or equal to , otherwise.
                class=""> <="secno">4.3.2.30.
                • Returnclass=""> , otherwise.
                <="secno">4.3.2.31.
                • Let signed interpretation of .
                • Let be the signed interpretation of . class=""> if is greater than or equal to , otherwise. 4.3.3. Floating-Point Operations

                  Floating-point arithmetic follows the IEEE 754-2008 standard, with the following qualifications:

                  • All operators use round-to-nearest ties-to-even, except where otherwise specified. Non-default directed rounding attributes are not supported.
                  • Following the recommendation that operators propagate NaN payloads from their operands is permitted but not required.
                  • All operators use “non-stop” mode, and floating-point exceptions are not otherwise observable. In particular, neither alternate floating-point exception handling attributes nor operators on status flags are supported. There is no observable difference between quiet and signalling NaNs.

                  Note

                  Some of these limitations may be lifted in future versions of WebAssembly.

                  4.3.3.1. Rounding

                  Rounding always is round-to-nearest ties-to-even, in correspondance with IEEE 754-2008 (Section 4.3.1).

                  An exact floating-point number is a rational number that is exactly representable as a floating-point number of given bit width .

                  A limit number for a given floating-point bit width is a positive or negative number whose magnitude is the smallest power of class=""> < representable as a floating-point number of width (that magnitclass=""> for and for ).

                  A candidate <

                  A caclass=""> of candidate numbers, such that no candidate number exists that lies between the two.

                  A real number is converted to a floating-point value of bit width

                  class=""> < If <
                  • If , thclass=""> .
                  • Else, return <
                  • Else if is aclass=""> <
                      class=""> , then return .
                    • Else, return <
                  • Else, return . class=""> <
                    4.3.3.2. NaN Propagation

                    When the result of a floating-point operator other than , , or computed as follows:

                    • If the payload of all NaN inputs to the operator is canonical (including the case that there are no NaN inputs), then the payload of the output is canonical as well.
                    • Otherwise the payload is picked non-determinsitically among all arithmetic NaNs; that is, its most significant bit is and all others are unspecified.

                    This non-deterministic result is expressed by the following auxiliary function producing a set of allowed outputs from a set of inputs:

                    class=""> 4.3.3.3.
                    • If either .
                    • Else if both < .
                    • Elseclass=""> are infinities of equal sign, then return that inficlass=""> is an infinity, theclass=""> and are zeroes of opposite sign, then rclass=""> < and are zeroes of equal sclass=""> < zero. class=""> or is a zero, then return the class=""> <
                    • Else class=""> and are values with the same magnitude bclass=""> <
                    • Else return the result of adding and , rounded to the nearest representable value.
                    4.3.3.4.
                    • If either .
                    • Else if both < .
                    • Else ifclass=""> are infinities of opposite sign, then return is an infinity, then return that infinitclass=""> is an infinity, then return that infinity negated. class=""> class=""> are zeroes of equal sign, then return positive zero. class=""> and are zeroes of opposite sclass=""> <
                    • Else if is a zero, then return <
                    • Else iclass=""> is a zero, then return Else if both and from , rounded to the nearest representable value.
                    .

                    class=""> <_1-z_2">4.3.3.5.
                    • If either .
                    • Else if one of .
                    • Eclass=""> are infinities of equal sign, then return positive class=""> < xxxxxxxxxxxxxxxxxxxxx/span> are infinities oclass=""> < return negative class=""> <
                    • Else if one of or is an infiniclass=""> Else if one of or < sign, then return negative infinity.
                    • Else if both and Else if both and are zeroes of opposite sclass=""> and rounded to the nearest representable value.
                    <">4.3.3.6.
                    • If either .
                    • Else if both < .
                    • Else if both and are zeroes, then return an element of <
                    • Else if < infinity and a value with equal sign, then return posiclass=""> <
                    • Else if is an infinity and
                    • Else if is an infinity and class=""> < sign, then return negative zeroclass=""> is a zero and a class=""> <, then return positive zero. class=""> is a zero and a value wiclass=""> is a zero and a valueclass=""> is a zero and a valuclass=""> < then return negative infinclass=""> Else return the result of dividing by rounded to the nearest representable value.
                    <">4.3.3.7.
                    • If either .
                    • Else if one of is a positive infinityclass=""> and are zeroes of opposite siclass=""> and .class=""> <
                      <">4.3.3.8.
                      • If either .
                      • Else if one of is a negative infinityclass=""> and are zeroes of opposite siclass=""> and . class=""> <
                        4.3.3.9.
                          class=""> .
                        • Else return with negated sign.
                        class=""> <.3.10.
                        • If Else if is an infinity, then return positive infinity.
                        • Else if < a zero, then return positive zero.class=""> is a positive valueclass=""> .
                        • Else return negclass=""> <
                        <.3.11.
                        • If Else if is an infinity, then return that infinity negated.
                        • Else if < is a zero, then return that zero nclass=""> <
                        • Else return negatedclass=""> <>
                          <4.3.3.12.
                          • If .
                          • Else if has a negative sign, then return anclass=""> is positive infinity, thclass=""> Else if <
                          <4.3.3.13.
                          • If .
                          • Else if is an infinity, then return .
                          • Else if <
                          • Else if class=""> , then reclass=""> <
                          • Else return the sclass=""> <>.
                          class=""> 4.3.3.14.
                          • If .
                          • Else if is an infinity, then return .
                          • Else if <
                          • Else if class=""> , then retclass=""> <
                          • Else return the laclass=""> <
                          class=""> 4.3.3.15.
                          • If .
                          • Else if is an infinity, then return .
                          • Else if <
                          • Else if class=""> , then retclass=""> <
                          • Else if is smaller than <
                          <="secno">4.3.3.16.
                          • If .
                          • Else if is an infinity, then return .
                          • Else if <
                          • Else if class=""> Elseclass=""> is smaller than but greater than or equclass=""> , then return negativclass=""> <
                          • Else return the integral value that is nearest to <; if two values are equally nclass=""> <4.3.3.17.
                            • If either .
                            • Else if both and are zeroes, then returnclass=""> . class=""> are the same value, class=""> <
                            • Else return <
                            <4.3.3.18.
                            • If either .
                            • Else if both and are zeroes, then returnclass=""> . class=""> are the same value, class=""> <
                            • Else return <
                            <4.3.3.19.

                            4.5.5. Invocation

                            Once a module has been instantiated, any exported function can be invoked externally via its function address in the store and an appropriaclass=""> of argument values <

                            Invocation may fail class=""> < href="index.html#syntax-functype">function type. Invocation can also result in a trap. It is up to the embedder to define how such conditions are reported.

                            Note

                            If the embedder API performs type checks itself, either statically or dynamically, before performing an invocation, then no failure other than traps can occur.

                            The following steps are performed:

                            1. Assert: exists.
                            2. Let .
                            3. Let .
                            4. If the length class=""> value type in and corresponding value in , do:
                              1. If for some , then: class=""> <
                              class=""> < the stack.
                            5. Invoke the function instance at addrclass=""> .

                            Once the function has returned, the following steps are executed:

                              < class="std std-ref">validation, values are on the top of the stack.
                            1. Pop from the stack.

                            The values 5. Binary Format

                            5.1. Conventions

                            The binary format for WebAssembly modules is a dense linear encoding of their abstract syntax. [1]

                            The format is defined by an attribute grammar whose only terminal symbols are bytes. A byte sequence is a well-formed encoding of a module if and only if it is generated by the grammar.

                            Each production of this grammar has exactly one synthesized attribute: the abstract syntax that the respective byte sequence encodes. Thus, the attribute grammar implicitly defines a decoding function.

                            Except for a few exceptions, the binary grammar closely mirrors the grammar of the abstract syntax.

                            Note

                            Some phrases of abstract syntax have multiple possible encodings in the binary format. For example, numbers may be encoded as if they had optional leading zeros. Implementations of decoders must support all possible alternatives; implementations of encoders can pick any allowed encoding.

                            The recommended extension for files containing WebAssembly modules in binary format is “” and the recommended Media Type is “”.

                            class=""> <"fn-backref" href="#id1">[1] Additional encoding layers – for example, introducing compression – may be defined on top of the basic representation defined here. However, such layers are outside the scope of the current specification.

                            5.1.1. Grammar

                            The following conventions are adopted in defining grammar rules for the binary format. They mirror the conventions used for abstract syntax. In order to distinguish symbols of the binary syntax from symbols of the abstract syntax, font is adopted for the former.

                            • Terminal symbols are bytes expressed in hexaclass=""> .
                            • Nonterminal symbols are written in typewriter font: .
                            • is a sequenceclass=""> .
                            • is aclass=""> . (This class=""> is not rclass=""> <
                            • . (This is aclass=""> where .) class=""> denotes the same langclass=""> , but alclass=""> to tclass=""> <
                            • Productions are wriclass=""> , where each in the given case, usually from attribute varclass=""> < augmented by side conditclass=""> <

                              Note

                              For example, the binary grammar for value types is given as follows:

                              encodes the typclass=""> , and sclass="">

                              class=""> limits is defined as follows:

                              value, or the byte nonterminals, which in this case are the class=""> unsigned inteclass="">

                              5.1.2. Auxiliary Notation

                              When dealing with binary encodings the following notation is also used:

                              • denotes the empty byte sequence.
                              • is the length of the byte sequence generated from the production in a derivation.
                              class=""> <">

                              <="secno">5.1.3. Vectors

                              Vectors are encoded with their length followed by the encoding of their element sequence.

                              <2" id="values⑥">5.2. Values

                              5.2.1. Bytes

                              Bytes encode themselves.

                              <="integers⑤">5.2.2. Integers

                              All integers are encoded using the LEB128 variable-length integer encoding, in either unsigned or signed variant.

                              Unsigned integers are encoded in unsigned LEB128 format. As an additional constraint, the total number of bytes encoding a value of type must not exceed bytes.

                              must not exceed bytes.

                              and encodings restrict the encodiclass=""> < “trailing zeros” are still allowed within these bounds. Fclass=""> are both well-formed encodings for the value and of termiclass=""> <> for negative ones. For example, is malformed as a are malformeclass=""> class=""> < <">5.2.3. Floating-Point

                              Floating-point values are encoded directly by their IEEE 754-2008 bit pattern in little endian byte order:

                              <5.2.4. Names

                              Names are encoded as a vector of bytes containing the Unicode UTF-8 encoding of the name’s code point sequence.

                              5.3. Types

                              5.3.1. Value Types

                              Value types are encoded by a single byte.

                              type indices. Thus, the binary format for types corresponds to the encodings of small negative values, so that they can coexist with (positive) type indices in the future.

                              5.3.2. Result Types

                              The only result types occurring in the binary format are the types of blocks. These are encoded in special compressed form, by either the byte indicating the empty type or as a single value type.

                              <

                              5.3.3. Function Types

                              Function types are encoded by the byte followed by the respective vectors of parameter and result types.

                              <"content">Limits

                              Limits are encoded with a preceding flag indicating whether a maximum is present.

                              Memory Types

                              Memory types are encoded with their limits.

                              5.3.6. Table Types

                              Table types are encoded with their limits and a constant byte indicating their element type.

                              5.3.7. Global Types

                              Global types are encoded by their value type and a flag for their mutability.

                              5.4. Instructions

                              Instructions are encoded by opcodes. Each opcode is represented by a single byte, and is followed by the instruction’s immediate arguments, where present. The only exception are structured control instructions, which consist of several opcodes bracketing their nested instruction sequences.

                              Note

                              Gaps in the byte code ranges for encoding instructions are reserved for future extensions.

                              5.4.1. Control Instructions

                              Control instructions have varying encodings. For structured instructions, the instruction sequences forming nested blocks are terminated with explicit opcodes for and .

                              < \[\begin{split}\begin{array}{llclll} \def\mathdef846#1{{}}\mathdef846{instruction} & \href{../binary/instructions.html#binary-instr}{\mathtt{instr}} &::=& \def\mathdef903#1{\mathtt{0x#1}}\mathdef903{00} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{unreachable}} \\ &&|& \def\mathdef904#1{\mathtt{0x#1}}\mathdef904{01} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{nop}} \\ &&|& \def\mathdef905#1{\mathtt{0x#1}}\mathdef905{02}~~\mathit{rt}{:}\href{../binary/types.html#binary-blocktype}{\mathtt{blocktype}}~~(\mathit{in}{:}\href{../binary/instructions.html#binary-instr}{\mathtt{instr}})^\ast~~\def\mathdef906#1{\mathtt{0x#1}}\mathdef906{0B} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{block}}~\mathit{rt}~\mathit{in}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ &&|& \def\mathdef907#1{\mathtt{0x#1}}\mathdef907{03}~~\mathit{rt}{:}\href{../binary/types.html#binary-blocktype}{\mathtt{blocktype}}~~(\mathit{in}{:}\href{../binary/instructions.html#binary-instr}{\mathtt{instr}})^\ast~~\def\mathdef908#1{\mathtt{0x#1}}\mathdef908{0B} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{loop}}~\mathit{rt}~\mathit{in}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ &&|& \def\mathdef909#1{\mathtt{0x#1}}\mathdef909{04}~~\mathit{rt}{:}\href{../binary/types.html#binary-blocktype}{\mathtt{blocktype}}~~(\mathit{in}{:}\href{../binary/instructions.html#binary-instr}{\mathtt{instr}})^\ast~~\def\mathdef910#1{\mathtt{0x#1}}\mathdef910{0B} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{if}}~\mathit{rt}~\mathit{in}^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{else}}~\epsilon~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ &&|& \def\mathdef911#1{\mathtt{0x#1}}\mathdef911{04}~~\mathit{rt}{:}\href{../binary/types.html#binary-blocktype}{\mathtt{blocktype}}~~(\mathit{in}_1{:}\href{../binary/instructions.html#binary-instr}{\mathtt{instr}})^\ast~~ \def\mathdef912#1{\mathtt{0x#1}}\mathdef912{05}~~(\mathit{in}_2{:}\href{../binary/instructions.html#binary-instr}{\mathtt{instr}})^\ast~~\def\mathdef913#1{\mathtt{0x#1}}\mathdef913{0B} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{if}}~\mathit{rt}~\mathit{in}_1^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{else}}~\mathit{in}_2^\ast~\href{../syntax/instructions.html#syntax-instr-control}{\mathsf{end}} \\ &&|& \def\mathdef914#1{\mathtt{0x#1}}\mathdef914{0C}~~l{:}\href{../binary/modules.html#binary-labelidx}{\mathtt{labelidx}} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br}}~l \\ &&|& \def\mathdef915#1{\mathtt{0x#1}}\mathdef915{0D}~~l{:}\href{../binary/modules.html#binary-labelidx}{\mathtt{labelidx}} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_if}}~l \\ &&|& \def\mathdef916#1{\mathtt{0x#1}}\mathdef916{0E}~~l^\ast{:}\href{../binary/conventions.html#binary-vec}{\mathtt{vec}}(\href{../binary/modules.html#binary-labelidx}{\mathtt{labelidx}})~~l_N{:}\href{../binary/modules.html#binary-labelidx}{\mathtt{labelidx}} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{br\_table}}~l^\ast~l_N \\ &&|& \def\mathdef917#1{\mathtt{0x#1}}\mathdef917{0F} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{return}} \\ &&|& \def\mathdef918#1{\mathtt{0x#1}}\mathdef918{10}~~x{:}\href{../binary/modules.html#binary-funcidx}{\mathtt{funcidx}} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call}}~x \\ &&|& \def\mathdef919#1{\mathtt{0x#1}}\mathdef919{11}~~x{:}\href{../binary/modules.html#binary-typeidx}{\mathtt{typeidx}}~~\def\mathdef920#1{\mathtt{0x#1}}\mathdef920{00} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-control}{\mathsf{call\_indirect}}~x \\ \end{array}\end{split}\]

                              Note

                              The opcode in the encoding of an

                              instruction may be used to index additional tables.

                              class=""> 5.4.2. Parametric Instructions

                              Parametric instructions are represented by single byte codes.

                              \[\begin{split}\begin{array}{llclll} \def\mathdef846#1{{}}\mathdef846{instruction} & \href{../binary/instructions.html#binary-instr}{\mathtt{instr}} &::=& \dots \\ &&|& \def\mathdefclass=""> <} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{drop}} \\ &&|& \def\mathdef923#1{\mathtt{0x#1}}\mathdef923{1B} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}} \\ \end{array}\end{split}\]

                              5.4.3. Variable Instructions

                              Variable instructions are represented by byte codes followed by the encoding of the respective index.

                              \[\begin{split}\begin{array}{llclll} \def\mathdef846#1{{}}\mathdef846{instruction} & \hrclass="">

                              5.4.4. Memory Instructions

                              Each variant of memory instruction is encoded with a different byte code. Loads and stores are followed by the encoding of their immediate.

                              \[\begin{split}\begin{array}{llclll}class="">
                              and instructions may be used to index additional memoriesclass=""> class=""> 5.4.5. Numeric Instructions

                              All variants of numeric instructions are represented by separate byte codes.

                              The instructions are followed by the respective literal.

                              Expressions

                              Expressions are encoded by their instruction sequence terminated with an explicit opcode for .

                              The binary encoding of modules is organized into sections. Most sections correspond to one component of a module record, except that function definitions are split into two sections, separating their type declarations in the function section from their bodies in the code section.

                              Note

                              This separation enables parallel and streaming compilation of the functions in a module.

                              5.5.1. Indices

                              All indices are encoded with their respective value.

                              Sections

                              Each section consists of

                              • a one-byte section id,
                              • the size of the contents, in bytes,
                              • the actual contents, whose structure is depended on the section id. class="">

                                The following parameterized grammar rule defines the generic structure of a section with id and contents described by the grammar .

                                is interpreted as the empty vector.

                                class="">

                                Note

                                Other than for unknown custom sections, the is not required for decoding, but can be used to skip sections when navigating through a binary. The module is malformed if the size does not match the length of the binary contents .

                                class=""> <
                                Id Section
                                0 custom section
                                1 type section
                                2 import section
                                3 function section
                                4 table section
                                5 memory section
                                6 global section
                                7 export section
                                8 start section
                                9 element section
                                10 code section
                                11 data section

                                5.5.3. Custom Section

                                Custom sections have the id 0. They are intended to be used for debugging information or third-party extensions, and are ignored by the WebAssembly semantics. Their contents consist of a name further identifying the custom section, followed by an uninterpreted sequence of bytes for custom use.

                                < invalidate the module.

                                5.5.4. Type Section

                                The type section has the id 1. It decodes into a vector of function types that represent the component of a module.

                                <5" id="import-section①">5.5.5. Import Section

                                The import section has the id 2. It decodes into a vector of imports that represent the component of a module.

                                Function Section

                                The function section has the id 3. It decodes into a vector of type indices that represent the fields of the functions in the module. The fields of the respective functions are encoded separately in the <

                                5.5.7. Table Section

                                The table section has the id 4. It decodes into a vector of tables that represent the component of a module.

                                <>5.5.8. Memory Section

                                The memory section has the id 5. It decodes into a vector of memories that represent the component of a module.

                                5.5.9. Global Section

                                The global section has the id 6. It decodes into a vector of globals that represent the component of a module.

                                < id="export-section①">5.5.10. Export Section

                                The export section has the id 7. It decodes into a vector of exports that represent the component of a module.

                                5.5.11. Start Section

                                The start section has the id 8. It decodes into an optional start function that represents the component of a module.

                                5.5.12. Element Section

                                The element section has the id 9. It decodes into a vector of element segments that represent the component of a module.

                                < data-level="5.5.13" id="code-section①">5.5.13. Code Section

                                The code section has the id 10. It decodes into a vector of code entries that are pairs of value type vectors and expressions. They represent the and field of the functionsclass=""> module. The function section.

                                The encodclass=""> <

                              • the size of the function code in bytes,
                              • the actual function code, which in turn consists of
                                  class=""> expression.

                              Local declarations are compressed into a vector whose entries consist of

                              • a count,
                              • a value type, class=""> vector class=""> <
                                <

                                Note

                                Like with sections, the code is not needed for decoding, but can be used to skip functions when navigating through a binary. The module is malformed if a size does not match the length of the respective function code.

                              5.5.14. Data Section

                              The data section has the id 11. It decodes into a vector of data segments that represent the component of a module.

                              5.5.15. Modules

                              The encoding of a module starts with a preamble containing a 4-byte magic number and a version field. The current version of the WebAssembly binary format is 1.

                              The preamble is followed by a sequence of sections. Custom sections may be inserted at any place in this sequence, while other sections must occur at most once and in the prescribed order. All sections can be empty. The lengths of vectors produced by the (possibly empty) function and code section must match up.

                              6. Text Format

                              6.1. Conventions

                              The textual format for WebAssembly modules is a rendering of their abstract syntax into S-expressions.

                              Like the binary format, the text format is defined by an attribute grammar. A text string is a well-formed description of a module if and only if it is generated by the grammar. Each production of this grammar has at most one synthesized attribute: the abstract syntax that the respective character sequence expresses. Thus, the attribute grammar implicitly defines a parsing function. Some productions also take a context as an inherited attribute that records bound identifers.

                              Except for a few exceptions, the core of the text grammar closely mirrors the grammar of the abstract syntax. However, it also defines a number of abbreviations that are “syntactic sugar” over the core syntax.

                              The recommended extension for source files containing WebAssembly modules in text format is “”. Files with this extension are assumed to be encoded in UTF-8, as per Unicode (Section 2.5).

                              6.1.1. Grammar

                              The following conventions are adopted in defining grammar rules for the text format. They mirror the conventions used for abstract syntax and for the binary format. In order to distinguish symbols of the textual syntax from symbols of the abstract syntax, font is adopted for the former.

                              • Terminal symbols are either literal strings of characters enclosed in quotes: Unicode code points: <ASCII subset of Uniclass=""> < font: .
                              • is a sequence of iterations of .
                              • is a possibly emclass=""> . (This is a shorthaclass=""> used whereclass=""> is not relevant.) class=""> iclass=""> . (This isclass=""> where .) class=""> is an optional occurrclass=""> . (This is a shorthand for where <
                              • , but also binds theclass=""> to the attributeclass=""> <>Productions are written < each isclass=""> < is synthesized for < the given case, usually from attribute variables boundclass=""> < expansion of the production into many separate cases.
                              class=""> <"simple" id="text-syntactic">
                            • A distinction is made between lexical and syntactic productions. For the latter, arbitrary white space is allowed in any place where the grammar contains spaces. The productions defining lexical syntax and the syntax of values are considered lexical, all others are syntactic.

                            Note

                            For example, the textual grammar for value types is given as follows:

                            <
                            unsigned integers

                            6.1.2. Abbreviations

                            In addition to the core grammar, which corresponds directly to the abstract syntax, the textual syntax also defines a number of abbreviations that can be used for convenience and readability.

                            Abbreviations are defined by rewrite rules specifying their expansion into the core syntax:

                            These expansions are assumed to be applied, recursively and in order of appearance, before applying the core grammar rules to construct the abstract syntax.

                            class="">

                            6.1.3. Contexts

                            The text format allows to use symbolic identifiers in place of indices. To resolve these identifiers into concrete indices, some grammar production are indexed by an identifier context as a synthesized attribute that records the declared identifiers in each index space. In addition, the context records the types defined in the module, so thaclass=""> parameter indices can be computed for functions.

                            It is convenient to define identifier contexts as records with abstract syntax as follows:

                            ) entries in these lists.

                            An identifier context is well-formed if no index space contains duplicate identifiers.

                            <">6.1.3.1. Conventions

                            To avoid unnecessary clutter, empty components are omitted when writing out identifier contexts. For example, the record is shorthand for an identifier context whose components are all empty.

                            class="">

                            6.1.4. Vectors

                            Vectors are written as plain sequences, but with a restriction on the length of these sequence.

                            6.2. Lexical Format

                            6.2.1. Characters

                            The text format assigns meaning to source text, which consists of a sequence of characters. Characters are assumed to be represented as valid Unicode (Section 2.4) code points.

                            or string literals, the rest of the grammar is formed exclusively from the characters supported by the 7-bit ASCII subset of Unicode.

                            6.2.2. Tokens

                            The character stream in the source text is divided, from left to right, into a sequence of tokens, as defined by the following grammar.

                            < class="reference internal" href="#text-space">white space, but except for strings, they cannot themselves contain whitespace.

                            The set of keyword tokens is defined implicitly, by all occurrences of a terminal symbol in literal form in a syntactic production of this chapter.

                            Any token that does notclass="">

                            Note

                            The effect of defining the set of reserved tokens is that all tokens must be separated by either parentheses or white space. For example, is a single reserved token. Consequently, it is not recognized as two separate tokens and , but instead disallowed. This property of tokenization is not affected by the fact that class=""> <

                            class=""> <-space">

                            6.2.3. White Space

                            White space is any sequence of literal space characters, formatting characters, or comments. The allowed formatting characters correspond to a subset of the ASCII format effectors, namely, horizontal tabulation (), line feed (), and carriage return (

                            6.2.4. Comments

                            A comment can either be a line comment, started with a double semicolon and extending to the end of the line, or a block comment, enclosed in delimiters

                            < the grammar such that only well-bracketed uses ofclass="">

                            6.3. Values

                            The grammar productions in this section define lexical syntax, hence no white space is allowed.

                            6.3.1. Integers

                            All integers can be written in either decimal or hexadecimal notation. In both cases, digits can optionally be separated by underscores.

                            6.3.2. Floating-Point

                            Floating-point values can be represented in either decimal or hexadecimal notation.

                            ), but it may be rounded to the nearest representable value.

                            <

                            Rounding can be prevented by using hexadecimal notation with no more significant bits than supported by the required type.

                            Floating-point values may also be written as constants for infinity or canonical NaN (not a number). Furthermore, arbitrary NaN values may be expressed by providing an explicit payload value.

                            <>Strings

                            Strings denote sequences of bytes that can represent both textual and binary data. They are enclosed in quotation marks and may contain any character other than ASCII control characters, quotation marks (), or backslash (), except when expressed with an escape sequence.

                            class=""> , which represent raw bytes of the respective value.

                            Names are strings denoting a literal character sequence. A name string must form a valid UTF-8 encoding as defined by Unicode (Section 2.5) that is interpreted as a string of Unicode code points.

                            6.3.5. Identifiers

                            Indices can be given in both numeric and symbolic form. Symbolic identifiers that stand in lieu of indices start with , followed by any sequence of printable ASCII characters that does not containclass="">

                            The expansion rules of some abbreviations require insertion of a fresh identifier. That may be any syntactically valid identifier that does not already occur in the given source text.

                            6.4. Types

                            6.4.1. Value Types

                            Result Types
                            <

                            6.4.3. Function Types

                            <

                            Multiple anonymous parameters or results may be combined into a single declaration:

                            Limits
                            Memory Types
                            6.4.6. Table Types

                            6.4.7. Global Types

                            6.5. Instructions

                            Instructions are syntactically distinguished into plain and structured instructions.

                            6.5.1. Labels

                            Structured control instructions can be annotated with a symbolic label identifier. They are the only symbolic identifiers that can be bound locally in an instruction sequence. The following grammar handles the corresponding update to the identifier context by composing the context with an additional label entry.

                            6.5.2. Control Instructions

                            Structured control instructions can bind an optional symbolic label identifier. The same label identifier may optionally be repeated after the corresponding and pseudo instructions, to indicate the matching delimiters.

                            must be empty in the rule for enforces that no identifier can be bound in any < class="heading settled" data-level="6.5.2.1" id="abbreviatioclass="">

                            The keyword of an instruction can be omitted if the following instruction sequence is empty. <">6.5.3. Parametric Instructions

                            \[\begin{split}\begin{array}{llclll} \def\mathdef2368#1{{}}\mathdef2368{instruction} & \href{../text/instructions.html#text-plaininstr}{\mathtt{plaininstr}}_I &::=& \dots \\ &&|& \def\mathdef2447#1class=""> <}\mathdef2447{drop} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{drop}} \\ &&|& \def\mathdef2448#1{\mbox{‘}\mathtt{#1}\mbox{’}}\mathdef2448{select} &\Rightarrow& \href{../syntax/instructions.html#syntax-instr-parametric}{\mathsf{select}} \\ \end{array}\end{split}\]

                            6.5.4. Variable Instructions

                            \[\begin{split}\begin{array}{llclll} \def\mathdef2368#1{{}}\mathdef2368{instruction} & \href{../text/instructiclass="">

                            6.5.5. Memory Instructions

                            The offset and alignment immediates to memory instructions are optional. The offset defaults to , the alignment to the storage size of the respective memory access, which is its natural alignment. Lexically, an or phrase is considered a single .

                            <. Numeric Instructions
                            <& \phantom{thisisenclass="">
                            <=}& \phantom{thisisclass="">
                            Folded Instructions

                            Instructions can be written as S-expressions by grouping them into folded form. In that notation, an instruction is wrapped in parentheses and optionally includes nested folded instructions to indicate its operands.

                            In the case of block instructions, the folded form omits the delimiter. For instructions, both branches have to wrapped into nested S-expressions, headclass=""> .

                            The set of all phrases defined by the following abbreviations reclass="">

                            <

                            6.5.8. Expressions

                            Expressions are written as instruction sequences. No explicit keyword is included, since they only occur in bracketed positions.

                            6.6.1. Indices

                            Indices can be given either in raw numeric form or as symbolic identifiers when bound by a respective construct. Such identifiers are looked up in the suitable space of the identifier context .

                            <>Types

                            Type definitions can bind a symbolic type identifier.

                            A type use is a reference to a type definition. It may optionally be augmented by explicit inlined parameter and result declarations. That allows binding symbolic identifiers to name the local indices of parameters. If inline declarations are given, then their types must match the referenced function type.

                            and the updated including possible parameter identifiers. The following auxiliary function extracts optional identifiers from parameters:

                            . However, in that case, they also produce the same results, so that the choice is immaterial.

                            The class=""> ensures that the parameters do not contain duplicate identifier.

                            6.6.3.1. Abbreviations

                            A may also be replaced entirely by inline parameter and < case, a type index is automatically inserted:

                            . If no such index exists, then a new type definition of the form

                            6.6.4. Imports

                            The descriptors in imports can bind a symbolic function, table, memory, or global identifier.

                            <

                            As an abbreviation, imports may also be specified inline with function, table, memory, or global definitions; see the respective sections.

                            6.6.5. Functions

                            Function definitions can bind a symbolic function identifier, and local identifiers for its parameters and locals.

                            <

                            ensures that parameters and locals do not contain duplicate identifiers.

                            <②">
                            6.6.5.1. Abbreviations

                            Multiple anonymous locals may be combined into a single declaration:

                            < xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxclass="">

                            <">6.6.6. Tables

                            Table definitions can bind a symbolic table identifier.

                            6.6.6.1. Abbreviations

                            An element segment can be given inline with a table definition, in which case the limits of the table type are inferred from the length of the given segment:

                            <

                            6.6.7. Memories

                            Memory definitions can bind a symbolic memory identifier.

                            6.6.7.1. Abbreviations

                            A data segment can be given inline with a memory definition, in which case the limits of the memory type are inferred from the length of the data, rounded up to page size:

                            <

                            6.6.8. Globals

                            Global definitions can bind a symbolic global identifier.

                            6.6.8.1. Abbreviations

                            Globals can be defined as imports or exports inline:

                            <> 6.6.9. Exports

                            The syntax for exports mirrors their abstract syntax directly.

                            <

                            As an abbreviation, exports may also be specified inline with function, table, memory, or global definitions; see the respective sections.

                            6.6.10. Start Function

                            A start function is defined in terms of its index.

                            grammar.

                            6.6.11. Element Segments

                            Element segments allow for an optional table index to identify the table to initialize. When omitted, is assumed.

                            table identifier resolving to the same value.

                            6.6.11.1. Abbreviations

                            As an abbreviation, element segments may also be specified inline with table definitions; see the respective section.

                            6.6.12. Data Segments

                            Data segments allow for an optional memory index to identify the memory to initialize. When omitted, is assumed. The data is written as a string, which may be split up into a possibly empty sequence of individual string literals.

                            <-id">memory identifier resolving to the same value.

                            6.6.12.1. Abbreviations

                            As an abbreviation, data segments may also be specified inline with memory definitions; see the respective section.

                            6.6.13. Modules

                            A module consists of a sequence of fields that can occur in any order. All definitions and their respective bound identifiers scope over the entire module, including the text preceding them.

                            A module may optionally bind an identifier that names the module. The name serves a documentary role only.

                            Note

                            Tools may include the module name in the name section of the binary format.

                            is defined if and only if

                            • <
                            • imports must occur before any regular definition of a function, table, memory, or global, thereby maintaining the ordering of the respective index spaces.

                              The well-formedness condition on in the grammar for ensures that no namespace contains duplicate identifiers.

                            The definition of the initial

                            <

                            In a source file, the toplevel surrounding the module body may be omitted.

                            7. Appendix

                            7.1. Embedding

                            A WebAssembly implementation will typically be embedded into a host environment. An embedder implements the connection between such a host environment and the WebAssembly semantics as defined in the main body of this specification. An embedder is expected to interact with the semantics in well-defined ways.

                            This section defines a suitable interface to the WebAssembly semantics in the form of entry points through which an embedder can access it. The interface is intended to be complete, in the sense that an embedder does not need to reference other functional parts of the WebAssembly specification directly.

                            Note

                            On the other hand, an embedder does not need to provide the host environment with access to all functionality defined in this interface. For example, an implementation may not support parsing of the text format.

                            In the description of the embedder interface, syntactic classes from the abstract syntax and the runtime’s abstract machine are used as names for variables that range over the possible objects from that class. Hence, these syntactic classes can also be interpreted as types.

                            Failure of an interface operation is indicated by an auxiliary syntactic class:

                            <

                            Note

                            Errors are abstract and unspecific with this definition. Implementations can refine it to carry suitable classifications and diagnostic messages.

                            7.1.1. Store

                            7.1.1.1.
                            1. Return thclass=""> .
                            Modules
                            7.1.2.1. byte sequence as a according to the , then return .
                          • Else, return .
                          • Else, return .
                          • Else, return <
                            7.1.2.4.
                            1. Try instantiating in with external vaclass="">
                              1. If it succeeds with a , then let be .
                              2. Else, let <
                              3. Return thclass="">
                                7.1.2.5. <
                                1. Assert: is valid with external import types .
                                2. Let <
                                3. Assert: the length of <
                                4. For each <
                                  class=""> 7.1.2.6. Assert: is valid with external import types .
                                5. Let <
                                6. Assert: the length of <
                                7. For each <
                                  class=""> . class="">
                                  Exports
                                7.1.3.1. <
                                1. Assert: due to validity of the module instance , all its export names are different.
                                2. If there exists aclass=""> in such that < , then:
                                    < .
                                3. Else, return Functions
                                7.1.4.1.
                                1. Let be the result of allocating a host function in function type .
                                2. Return the new store paired with <
                                pre- and post-conditions required for a function instance with type <>.

                                Regular (non-host) function instances can only be created indirectly through <>

                                7.1.4.2. < exists.
                              4. Assert: the is valid with .
                              5. Return . <-href-exec-runtimehtmlsyntax-funcaddrmathitfuncaddr-href-exec-runtimehtmlsyntax-valmathitvalast--href-exec-runtimehtmlsyntax-storemathitstore-href-exec-runtimehtmlsyntax-valmathitvalast--href-appendix-embeddinghtmlembed-errormathiterror">7.1.4.3.
                                1. Assert: exists.
                                2. Try with values as arclass=""> <
                                  1. If it succeeds with as results, then let be .
                                  2. Else it has traclass=""> . class=""> <
                                    1. Return thclass=""> <="section" id="tables⑨">

                                      7.1.5. Tables

                                      7.1.5.1.
                                      1. Let be the result of allocating a table in table type .
                                      class=""> 7.1.5.2. exists.
                                    2. Assert: the is valid with .
                                    3. Return . class=""> 7.1.5.3. <
                                      1. Assert: exists.
                                      2. Assert: is a non-neclass=""> <> .
                                      3. If is larger than or equalclass=""> . class=""> <
                                        7.1.5.4.
                                      1. Assert: exists.
                                      2. Assert: is a non-neclass=""> <> .
                                      3. If is larger than or equalclass=""> . class=""> < . class=""> 7.1.5.5. exists.
                                      4. Return the length of . 7.1.5.6.
                                      5. Assert: exists.
                                      6. Assert: is a non-neclass=""> by elements:
                                          < <>
                                          Memories
                                          7.1.6.1.
                                        1. Let be the result of allocating a memory in memory type .
                                        class=""> 7.1.6.2. exists.
                                      7. Assert: the is valid with .
                                      8. Return .
                                      class=""> 7.1.6.3. <="arabic simple">
                                    4. Assert: exists.
                                    5. Assert: is a non-negativeclass=""> < .
                                    6. If is larger than or equal to thclass=""> . class="">
                                      7.1.6.4.
                                      1. Assert: exists.
                                      2. Assert: is a non-negativeclass=""> < .
                                      3. If is larger than or equal to thclass=""> . class=""> <
                                      7.1.6.5. exists.
                                    7. Return the length of divided by the 7.1.6.6.
                                    8. Assert: exists.
                                    9. Assert: is a non-negativeclass=""> < by .
                                  Globals
                                  7.1.7.1.
                                  1. Let be the result of allocating a global in global type .
                                  2. Return the new store paired with <>
                                    7.1.7.2.
                                  3. Assert: exists.
                                  4. Assert: the is valid with .
                                  5. Return . class=""> 7.1.7.3. exists.
                                  6. Let beclass=""> .
                                  7. Return the <-globaladdrmathitglobaladdr-href-exec-runtimehtmlsyntax-valmathitval--href-exec-runtimehtmlsyntax-storemathitstore--href-appendix-embeddinghtmlembed-errormathiterror">7.1.7.4.
                                    1. Assert: exists.
                                    2. Let be the .
                                    3. If < xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxclass=""> 7.2. Implementation Limitations

                                      Implementations typically impose additional restrictions on a number of aspects of a WebAssembly module or execution. These may stem from:

                                      • physical resource limits,
                                      • constraints imposed by the embedder or its environment,
                                      • limitations of selected implementation strategies.

                                      This section lists allowed limitations. Where restrictions take the form of numeric limits, no minimum requirements are given, nor are the limits assumed to be concrete, fixed numbers. However, it is expected that all implementations have “reasonably” large limits to enable common applications.

                                      Note

                                      A conforming implementation is not allowed to leave out individual features. However, designated subsets of WebAssembly may be specified in the future.

                                      7.2.1. Syntactic Limits

                                      7.2.1.1. Structure

                                      An implementation may impose restrictions on the following dimensions of a module:

                                      If the limits of an implementation are exceeded for a given module, then the implementation may reject the validation, compilation, or instantiation of that module with an embedder-specific error.

                                      Note

                                      The last item allows embedders that operate in limited environments without support for Unicode to limit the names of imports and exports to common subsets like ASCII.

                                      7.2.1.2. Binary Format

                                      For a module given in binary format, additional limitations may be imposed on the following dimensions:

                                      7.2.1.3. Text Format

                                      For a module given in text format, additional limitations may be imposed on the following dimensions:

                                      7.2.2. Validation

                                      An implementation may defer validation of individual functions until they are first invoked.

                                      If a function turns out to be invalid, then the invocation, and every consecutive call to the same function, results in a trap.

                                      Note

                                      This is to allow implementations to use interpretation or just-in-time compilation for functions. The function must still be fully validated before execution of its body begins.

                                      7.2.3. Execution

                                      Restrictions on the following dimensions may be imposed during execution of a WebAssembly program:

                                      If the runtime limits of an implementation are exceeded during execution of a computation, then it may terminate that computation and report an embedder-specific error to the invoking code.

                                      Some of the above limits may already be verified during instantiation, in which case an implementation may report exceedance in the same manner as for syntactic limits.

                                      Note

                                      Concrete limits are usually not fixed but may be dependent on specifics, interdependent, vary over time, or depend on other implementation- or embedder-specific situations or events.

                                  7.3. Validation Algorithm

                                  The specification of WebAssembly validation is purely declarative. It describes the constraints that must be met by a module or instruction sequence to be valid.

                                  This section sketches the skeleton of a sound and complete algorithm for effectively validating code, i.e., sequences of instructions. (Other aspects of validation are straightforward to implement.)

                                  In fact, the algorithm is expressed over the flat sequence of opcodes as occurring in the binary format, and performs only a single pass over it. Consequently, it can be integrated directly into a decoder.

                                  The algorithm is expressed in typed pseudo code whose semantics is intended to be self-explanatory.

                                  7.3.1. Data Structures

                                  The algorithm uses two separate stacks: the operand stack and the control stack. The former tracks the types of operand values on the stack, the latter surrounding structured control instructions and their associated blocks.

                                  type val_type = I32 | I64 | F32 | F64

                                  type opd_stack = stack(val_type | Unknown)

                                  type ctrl_stack = stack(ctrl_frame) type ctrl_frame = { label_types : list(val_type) end_types : list(val_type) height : nat unreachable : bool }

                                  For each value, the operand stack records its value type, or Unknown when the type is not known.

                                  For each entered block, the control stack records a control frame with the type of the associated label (used to type-check branches), the result type of the block (used to check its result), the height of the operand stack at the start of the block (used to check that operands do not underflow the current block), and a flag recording whether the remainder of the block is unreachable (used to handle stack-polymorphic typing after branches).

                                  Note

                                  In the presentation of this algorithm, multiple values are supported for the result types classifying blocks and labels. With the current version of WebAssembly, the list could be simplified to an optional value.

                                  For the purpose of presenting the algorithm, the operand and control stacks are simply maintained as global variables:

                                  var opds : opd_stack var ctrls : ctrl_stack

                                  However, these variables are not manipulated directly by the main checking function, but through a set of auxiliary functions:

                                  func push_opd(type : val_type | Unknown) = opds.push(type)

                                  func pop_opd() : val_type | Unknown = if (opds.size() = ctrls[0].height && ctrls[0].unreachable) return Unknown error_if(opds.size() = ctrls[0].height) return opds.pop()

                                  func pop_opd(expect : val_type | Unknown) : val_type | Unknown = let actual = pop_opd() if (actual = Unknown) return expect if (expect = Unknown) return actual error_if(actual =/= expect) return actual

                                  func push_opds(types : list(val_type)) = foreach (t in types) push_opd(t) func pop_opds(types : list(val_type)) = foreach (t in reverse(types)) pop_opd(t)

                                  Pushing an operand simply pushes the respective type to the operand stack.

                                  Popping an operand checks that the operand stack does not underflow the current block and then removes one type. But first, a special case is handled where the block contains no known operands, but has been marked as unreachable. That can occur after an unconditional branch, when the stack is typed polymorphically. In that case, an unknown type is returned.

                                  A second function for popping an operand takes an expected type, which the actual operand type is checked against. The types may differ in case one of them is Unknown. The more specific type is returned.

                                  Finally, there are accumulative functions for pushing or popping multiple operand types.

                                  Note

                                  The notation stack[i] is meant to index the stack from the top, so that ctrls[0] accesses the element pushed last.

                                  The control stack is likewise manipulated through auxiliary functions:

                                  func push_ctrl(label : list(val_type), out : list(val_type)) =  let frame = ctrl_frame(label, out, opds.size(), false) ctrls.push(frame)

                                  func pop_ctrl() : list(val_type) =  error_if(ctrls.is_empty())  let frame = ctrls.pop() pop_opds(frame.end_types) error_if(opds.size() =/= frame.height) return frame.end_types

                                  func unreachable() = opds.resize(ctrls[0].height) ctrls[0].unreachable := true

                                  Pushing a control frame takes the types of the label and result values. It allocates a new frame record recording them along with the current height of the operand stack and marks the block as reachable.

                                  Popping a frame first checks that the control stack is not empty. It then verifies that the operand stack contains the right types of values expected at the end of the exited block and pops them off the operand stack. Afterwards, it checks that the stack has shrunk back to its initial height.

                                  Finally, the current frame can be marked as unreachable. In that case, all existing operand types are purged from the operand stack, in order to allow for the stack-polymorphism logic in pop_opd to take effect.

                                  Note

                                  Even with the unreachable flag set, consecutive operands are still pushed to and popped from the operand stack. That is necessary to detect invalid examples like <

                                  7.3.2. Validation of Opcode Sequences

                                  The following function shows the validation of a number of representative instructions that manipulate the stack. Other instructions are checked in a similar manner.

                                  Note

                                  Various instructions not shown here will additionally require the presence of a validation context for checking uses of indices. That is an easy addition and therefore omitted from this presentation.

                                  func validate(opcode) = switch (opcode) case (i32.add) pop_opd(I32) pop_opd(I32) push_opd(I32)

                                  case (drop) pop_opd()

                                  case (select) pop_opd(I32) let t1 = pop_opd() let t2 = pop_opd(t1) push_opd(t2)

                                  case (unreachable)    unreachable()

                                  case (block t*) push_ctrl([t*], [t*])

                                  case (loop t*) push_ctrl([], [t*])

                                  case (if t*) push_ctrl([t*], [t*])

                                  case (end) let results = pop_ctrl() push_opds(results)

                                  case (else) let results = pop_ctrl() push_ctrl(results, results)

                                  case (br n)

                                       error_if(ctrls.size() < n)    pop_opds(ctrls[n].label_types)     unreachable()

                                  case (br_if n)

                                       error_if(ctrls.size() < n) pop_opd(I32)    pop_opds(ctrls[n].label_types)    push_opds(ctrls[n].label_types)

                                  case (br_table n* m)    error_if(ctrls.size() < m)     foreach (n in n*)       error_if(ctrls.size() < n || ctrls[n].label_types =/= ctrls[m].label_types) pop_opd(I32)     pop_opds(ctrls[m].label_types)     unreachable()

                                  Note

                                  It is an invariant under the current WebAssembly instruction set that an operand of Unknown type is never duplicated on the stack. This would change if the language were extended with stack operators like dup. Under such an extension, the above algorithm would need to be refined by replacing the Unknown type with proper type variables to ensure that all uses are consistent.

                                  7.4. Custom Sections

                                  This appendix defines dedicated custom sections for WebAssembly’s binary format. Such sections do not contribute to, or otherwise affect, the WebAssembly semantics, and like any custom section they may be ignored by an implementation. However, they provide useful meta data that implementations can make use of to improve user experience or take compilation hints.

                                  Currently, only one dedicated custom section is defined, the name section.

                                  7.4.1. Name Section

                                  The name section is a custom sections whose name string is itself . The name section should appear only once in a module, and only after the data section. text form.

                                  Note

                                  All names are represented in Unicode encoded in UTF-8. Names need not be unique.

                                  7.4.1.1. Subsections

                                  The data of a name section consists of a sequence of subsections. Each subsection consists of a

                                  • a one-byte subsection id,
                                  • the size of the contents, in bytes,
                                  • the actual contents, whose structure is depended on the subsection id.
                                  class=""> < Id Subsection 0 module name 1 function names 2 local names
                                  7.4.1.2. Name Maps

                                  A name map assigns names to indices in a given index space. It consists of a vector of index/name pairs in order of increasing index value. Each index must be unique, but the assigned names need not be.

                                  < where secondary indices are grouped by primary indices. It consists of a vector of primary index/name map pairs in order of increasing index value, where each name map in turn maps secondary indices to names. Each primary index must be unique, and likewise each secondary index per individual name map.

                                  <"content">Module Names

                                  The module name subsection has the id 0. It simply consists of a single name that is assigned to the module itself.

                                  Function Names

                                  The function name subsection has the id 1. It consists of a name map assigning function names to function indices.

                                  Local Names

                                  The local name subsection has the id 2. It consists of an indirect name map assigning local names to local indices grouped by function indices.

                                  < id="soundness①">7.5. Soundness

                                  The type system of WebAssembly is sound, implying both type safety and memory safety with respect to the WebAssembly semantics. For example:

                                  • All types declared and derived during validation are respected at run time; e.g., every local or global variable will only contain type-correct values, every instruction will only be applied to operands of the expected type, and every function invocation always evaluates to a result of the right type.
                                  • No memory location will be read or written except those explicitly defined by the program, i.e., as a local, a global, an element in a table, or a location within a linear memory.
                                  • There is no undefined behaviour, i.e., the execution rules cover all possible cases that can occur in a valid program, and the rules are mutually consistent.

                                  Soundness also is instrumental in ensuring additional properties, most notably, encapsulation of function and module scopes: no locals can be accessed outside their own function and no module components can be accessed outside their own module unless they are explicitly exported or imported.

                                  The typing rules defining WebAssembly validation only cover the static components of a WebAssembly program. In order to state and prove soundness precisely, the typing rules must be extended to the dynamic components of the abstract runtime, that is, the store, configurations, and administrative instructions. [1]

                                  7.5.1. Values and Results

                                  Values and results can be classified by value types and result types as follows.

                                  7.5.1.1. Values
                                  <
                                  <.html#syntax-result">Results
                                  7.5.2.6. Global Instances <"simple">
                                3. The global instance is valid with global type .
                          7.5.2.7. Export Instances
                        • The external value must be valid with some .
                        • Then the export instance is valid.
                        7.5.2.8. Module Instances
                        7.5.4.4. external memory value must be valid with some .
                      • The index must be smaller than or equal to < href="index.html#page-size"> 7.5.4.5.
                      • The instruction sequence must be valid with some type <> be the same context as result type prepended to the <
                      • Under context , the instruction sequence must be valid with type .
                      7.5.4.6. , the thread must be valid with class=""> .
                    <="content">Store Extension

                    Programs can mutate the store and its contained instances. Any such modification must respect certain invariants, such as not removing allocated instances or changing immutable definitions. While these invariants are inherent to the execution semantics of WebAssembly instructions and modules, host functions do not automatically adhere to them. Consequently, the required invariants must be stated as explicit constraints on the invocation of host functions. Soundness only holds when the embedder ensures these constraints.

                    The necessary constraints are codified by the notion of store extension: a store state extends state , written , when the following rules hold.

                    <

                    .

                    7.5.5.1. Store